FDL - Nuprl Lemma : bijection_restriction

Nuprl Lemma : bijection_restriction

k:

, f:(

k

k).
0<k

Bij(

k;

k; f)

f(k-1) = k-1

{f

(k-1)

(k-1) & Bij(

(k-1);

(k-1); f)}

Definitions Prop, {T}, S T, S T, x:A. B(x), i j < k, P & Q, t T, , AB, A, False, P Q, Bij(A; B; f), {i..j}, T, True, Dec(P), P Q, Inj(A; B; f), Surj(A; B; f), x:A. B(x)

Lemmas le wf, decidable int equal, nat wf, int seg wf, biject wf